The Jordan Curve Theorem (JCT) states that a simple closed curve divides theplane into exactly two connected regions. We formalize and prove the theorem inthe context of grid graphs, under different input settings, in theories ofbounded arithmetic that correspond to small complexity classes. The theory$V^0(2)$ (corresponding to $AC^0(2)$) proves that any set of edges that formdisjoint cycles divides the grid into at least two regions. The theory $V^0$(corresponding to $AC^0$) proves that any sequence of edges that form a simpleclosed curve divides the grid into exactly two regions. As a consequence, theHex tautologies and the st-connectivity tautologies have polynomial size$AC^0(2)$-Frege-proofs, which improves results of Buss which only apply to thestronger proof system $TC^0$-Frege.
展开▼
机译：乔丹曲线定理（JCT）指出，简单的闭合曲线将平面分为两个完全相连的区域。我们在网格图的上下文中，在不同的输入设置下，以对应于小型复杂性类的有界算术理论形式化并证明了该定理。理论$ V ^ 0（2）$（对应于$ AC ^ 0（2）$）证明形成不相交循环的任何一组边将网格划分为至少两个区域。理论$ V ^ 0 $（对应于$ AC ^ 0 $）证明了形成简单闭合曲线的任何边序列都将网格精确地划分为两个区域。结果，十六进制重言式和st-连通性重言式具有多项式大小$ AC ^ 0（2）$-Frege-proofs，这改善了仅适用于更强的证明系统$ TC ^ 0 $ -Frege的Bus结果。
展开▼
